Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from the state space explosion problem that makes them impractical for large scale systems and/or specifications. In this paper, we propose to use graph representation learning (GRL) for solving linear temporal logic (LTL) model checking, where the system and the specification are expressed by a B\"uchi automaton and an LTL formula respectively. A novel GRL-based framework OCTAL, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification in the latent space. The empirical experiments show that OCTAL achieves comparable accuracy against canonical SOTA model checkers on three different datasets, with up to $5\times$ overall speedup and above $63\times$ for satisfiability checking alone.

In the terminology of computer science, Concurrent Systems identify systems, either software, hardware or even biological systems, where sets of activities run in parallel with possible occasional interactions. A simple example of concurrent system is the Internet, which can be thought of as a set of computers, each one computing its independent activity, that often communicate to exchange some information. A further example is the railway system of a country, where many trains travel sharing tracks in an ordered way so that two trains can move at the same time along different tracks, whereas a single track (e.g, a platform in a train station) can only be used by a single train at a time. Furthermore, the large number of activities carried on by a single human cell form a biological concurrent system, that actually shares a number of similarities with the Internet. Compared to sequential systems, where a single action is executed at a time according to a sequential algorithm, concurrent systems raise new complex issues dealing with the ordering of action executions.